| Definitions | Rinit-v(x1), Reffect-f(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-discrete(A), P   Q, P  Q, Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), let x = a in b(x), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1),  b, Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1), (i = j), band(p; q), R-interface-compat(A; B), R-discrete_compat(A; B), R-frame-compat(A; B), R-base-domain(R), eq_bd(p; q), Rda(R), Rds(R), R-loc(R), True, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), A c B, P Q, ff, i <z j,   b, tl(l), i  z j, nth_tl(n;as), hd(l), prop{i:l}, guard(T), sq_type(T), l[i], ||as||, top, t.2, fpf-ap(f; eq; x), tt, eq_atom{$n:n}(x; y), atom2-deq, eqof(d), bor(p; q), t.1, Y, reduce(f; k; as), deq-member(eq; x; L), fpf-dom(eq; x; f), if b then t else f fi , id-deq, fpf-cap(f; eq; x; z),   x. t(x), decl-type{i:l}(ds; x), Id, t  T, l_all(L; T; x.P(x)), R-compat{i:l}(A; B), pairwise(x,y.P(x;y); L), es_realizer{i:l}, mkid{$x:ut2}, fpf-single(x; v), onceR{$a:ut2, $done:ut2}(i), Rlist(L), send_onceR{$done:ut2, $tg:ut2, $b:ut2, $done1:ut2}(T; A; f; l), R-Feasible{i:l}(R), normal-type{i:l}(T), P Q, IdLnk,  x:A. B(x),  ,  x:A. B(x), False, Unit, (x l), eq_id(a; b),  , P  Q, decidable(P), int_seg(i; j), x(s), decl-state(ds),  |
T), l:IdLnk.
